Flow-sensitive Typing - herp-technote

Flow-sensitive Typing
#型システム #TypeScript

型{推論,検査}にコントロールフローを利用する型システム｡
TypeScript, Typed Racket(c.f. occurrence typing)などが利用している｡
型版のsupercompilationっぽい

typescript
	function f(v : number | null) {
	  if (v !== null) {
	    // この中ではなんとvの型はnumberとして扱われる
	    ......
	  } else {
	  	// この中ではなんとvの型はnullとして扱われる
	  }
	}

Links
型システム
プログラムの振る舞いを[* 型]を用いて近似し､[* 静的に]安全性を保証する仕組み｡型なし､単相型､一階多相､n階多相､線形型､型関数､依存型など､強力な型があればあるほど静的に安全性を保証できる範囲が広がる一方､型の不一致が起きてないかどうかの計算が複雑になり､型が正しいかどうかの証明を与える必要があるなどのトレードオフがある｡

型システム
Lightweight Higher-kinded Polymorphism
#型システム #TypeScript #fp-ts高階型の無い型システムにおいて高階型をエンコードする方法｡defunctionalizationを応用して､HKTの高階型を関数､型適用を関数適用にそのまま当てはめる｡[** fp-tsにおける高階型][fp-ts]では`HKT`というinterfaceが用意されている｡作者が`Option`を題材に使い方を説明している｡
社内調査：Ladder of Functional Programming 〜関数型プログラミングのレベル分け〜
Higher Kinded Types
#型システム型を受け取って型を返す型 (`* → *`)｡高階型､Higher Rank Typesとも｡HKTと略される｡例えばHKTの無い[OCaml]では､`'a list` は[* 型ではなく型コンストラクタ]という扱いになっているが､HKTのある[Haskell](`List A` または `[A]`)では `* → *` という `A`型を受け取って`[A]`を返す[* 型]である｡式を取って式を返すという関数が式であるとさまざまな実りがある(c.f. [ラムダ計算])ように､型を受け取って型を返すという仕組みも型に含まれているとさまざまな嬉しさがある｡
モナド
#Haskell #型システム[**** 概要]計算エフェクト`m`がついている`a`型の値を扱うときに便利｡`(>>=) :: m a -> (a -> m b) -> m b` の左辺に値`m a`を入れると､右辺の関数`a -> m b`内では`a`型の(純粋な)値として扱うことができるようになる｡しかし`>>=`を多用すると [fp-ts]の`chain`のように､いわゆるコールバック地獄になって見た目がよろしくない｡
Haskell
TypeFamilies
型族 (indexed type families) を有効化する．型クラス (type class) が，データ型に対する関数のアドホック多相を提供するのに対し，型族は，データ型に型のアドホック多相を提供する．主に [/ associated type synonym] という機能を使うが，これは `class` 及び `instance` 構文以下に，関連付けられる型シノニムを `type HERP のアプリケーションにおいては，認証用に用いる識別子の型はたまたま `UserId` だが，他のアプリケーションでは `MemberId` かもしれないし，はたまたまったく異なるデータ型かもしれない．`TypeFamilies` 拡張を用いることによって，ユーザ側で起きうるこのような差異を吸収している．
value restriction
#型システム[*** 問題]非純粋･call by value･多相の3つが揃うとき大変なことが起こる｡今､value restrictionのないML方言と参照セルとリストコンストラクタを用意する｡let多相があると､let-boundなものを多相にすることができる｡`r`は多相なリスト`'a list`を持っているので`'a list ref` 型になる｡さて､`r`のリストの参照を更新していくわけだが
System F
#型システム #ラムダ計算[* 二階ラムダ計算] や [* 多相ラムダ計算] として知られる｡またこれを型システムに埋め込むことで強力な型を表現できる｡簡単な例として､よくある `id` 関数をSystem Fで表すとこのようになる｡[$ \mathit{id} = \Lambda a. \lambda x : a. x \rightarrow x][$ x]の[* 型を[$ a]でパラメタライズ] することで[* 多相性] を獲得している｡

TypeScript
Tech in HERP
HERPで使われている技術[** Languages][TypeScript][Haskell][** Web application frameworks]
fp-ts-contrib/lib/Do を用いた手続き型プログラミング
#fp-ts #TypeScript #モナド[** example]`Do(Monad)` でインスタンスを作り､メソッドチェインで変数環境を育てる｡[** operators]`L`(azy)がpostfixに付くoperatorは､それまでの計算エフェクトに依存した計算ができる｡
TypeScript 3.5
https://devblogs.microsoft.com/typescript/announcing-typescript-3-5/[takuma.icon][{ ちょっとずつ書いていきます][***** The Omit helper type]ある型から一部のkeyを取り除いた部分型を示す`Omit`が追加されます。`Omit<T, 'key'>`は`T`から`key`を除いた型を表す。[* 例]